% -*- prolog -*-
%
%  RichProlog 2
%
% Patrick Caldon, December 2002
%  2006 - rewritten for rp4
%
% This code is implemented as a set of macro expansions and 
% support predicates for a standard prolog supporting these 
% extensions, e.g. Yap 4.4 or Sicstus.  Currently it is tested
% and supported on Yap 4.4, and some limited testing has been
% done on Sicstus.  Porting to SWI should also be possible.
%

% TODO:
%
% - stream handler * DONE *
% - proper unification of subtypes * DONE *
% - finite domains - currently working, but needs early cutout * DONE *
% - new toplevel * DONE *
% - modularize * DONE *
% - proper parser * DONE *
% - handle exceptions properly * DONE *
% - implication rewrite * DONE *
% - bring together onot and rnot * DONE *
% - sort out precise condition for exist/univ variables in refut/non-refut parts. * DONE *
% - query macros * DONE *
% - BUG: propositional only queries fail 
% - incremental query * DONE * - but bugged! - but fixed & not tested!
% - simple table resize * DONE *

% - quick numerals
% - handle ^C exceptions (rather than sig_usr1)
% - complete matrix library
% - dynamic table resize
% - port to swi - part done ...
% - call counting modifications
%


% NOTES:
%  - predicates are split into two kinds, evidential and theoretical.
%  - theoretical predicates can be used in extended horn clauses, i.e.
%    horn clauses with arbitrary disjunction and conjuntion before the 
%    implication symbol
%  - evidential predicates are indicated by a preceeding "`" (i.e. 
%    quote) symbol;  these can only be used in limited circumstances.

/*
Queries:

queries are of the form ex(Varlist) all(Varlist) $\phi$(Vars) where 
$\phi$ is open (i.e. $\phi$ is the matrix of the prenex-form query).

Matrix restrictions:

$\phi$ is positive over some set $X$. All formulae in $X$ are
either theoretical atomic or formulae from another set $Y$.
Here $Y$ is the set of refutable formulae that is the negation
of positive formulae over the set theoretical atomic formulae 
and evidential basic formulae. 

Prefix restrictions:

Universally quanitfied variables can only appear in refutable clauses.

quantified.

Program Restrictions:

Programs contain either positive clauses of theoretical predicates or
ground basic clauses of evidential predicates.

Syntax (example):

theor2(X,Y) :- theor1([],[]); theor2([],[]). % <-- theoretical predicates only in program part

`observ(a).
not `observ(b).  % <-- "`" indicates an evidential predicate; negation is allowed.  

Execution model:

Queries are performed via two rounds of SLD resolution.  Suppose the
query is:

? ex(X), all(Y), theor1(X) , neg( theor2(X,Y) , `observ(Y)). 

First the query will be posed to the SLD engine:

? theor1(X).

which will result in some value for X, e.g. X=t.  A second
query will then be posed,
 
? neg( theor1(t) , neg( theor2(t,Y) , `observ(Y) )). 

(in this case, this is equivalent to the query ? theor2(t,Y) , `observ(Y).)

i.e. this will fail only if $\neg (\forall Y \neg (theor1(X) \wedge 
\neg  ( theor2(X,Y) \wedge `observ(Y) ) )) [t/X]$ is true.  

This second query must fail; if it succeeds, we backtrack to find 
some other term for X.  If (as we hope) it fails, we report t as a 
valid value for X. 

Query summary:

If positive($\phi$) and
  forall members $\psi$ of $\phi$
    not_refutable($\psi$) - variables in $\psi$ existentally quantified
    or
    refutable($\psi$)

where refutable(x) is defined by:

refutable(x) <=> 
	x = neg(y) 
        and
        forall members z of y
           theoretical_atomic(z) - (some) variables in z universally quantified
           or
           evidential(z) - (some) variables in z universally quantified


evidential(z) is true iff z is something out of the evidence set.
Note evidential stuff is in general basic, not atomic;

The rule can be abbreviated to the shorthand "*Universal* Variables 
only in the *Refutable* Part of the query". 

Implementation:

Theory parser:

First it is assumed that all predicates with a "`" symbol prepended are
evidential, and if a predicate is not evidential then it it theoretical.
This allows conventional Prolog programs to execute as normal.

A program is read in as usual, with a special "`" macro expansion defined.
This effectively executes the following code:

`P :- P =.. [Funct|Args],
      atom_concat(['$obs',Funct],NewFunct),
      Q =.. [NewFunct|Args],
      assert(Q).

not `P :- P =.. [Funct|Args],
	  atom_concat(['$negobs',Funct],NewFunct),
	  Q =.. [NewFunct|Args],
	  assert(Q).

Furthermore a check is made that no evidential predicates appear in
standard code.

A query is read in, evidential names transformed as before, and a
query executed in two steps (in pseudo-prolog):

query(X,Y,S) :- check_syntax(S),
	      transform_evidential(S,S0),
	      assert_refutable_parts(S0,S1),
	      call(S1),
	      \+ call(S0),
	      print(X).

Here "assert refutable parts" transforms all refutable parts of a 
query into a call to "true", so only the existential query is made if the
syntax is correct; furthermore its action should ground as far as is
practical the existentially quantified variables resulting in the
second query working as planned.

Type Unification Rules:

- A subtype may unify with a supertype; the resulting term will have
the subtype''s type.
- Two equivalent types may unify; the resultant term (as a convention)
will have the simplest type in terms of term depth.
- In generating the type graph, it is compiled into its transitive
closure, which is then used to check if unification is possible.

*/
:- module(richprolog,
	[query/5,
	rpdb/0,
	rp_handle_signal/0,
	rp_version/1,
	rp_last_result/1,
	evidential/1,
	all_in_set/3,
	list_profile/0]).

%:- source.
:- multifile neg/1.


prolog_type(yap):-
        predicate_property(yap_flag(_,_),built_in), !.
prolog_type(swi).

%:-	use_module(library(atts)).


%init(yap) :- 
%	yap_flag(unknown,error),
%	yap_flag(single_var_warnings,on),
%:-	use_module(library(random)).
%:-	use_module(library(terms)).
:-	use_module(library(lists)).
%:-	use_module(library(apply_macros)).
%:-	use_module(library(assoc)).
%:-	setrand(rand(26,2,1976)).



init(swi) :- use_module(library(lists)),
	     use_module('apply_macros.swi'),
	     dynamic(set_value/2),
	     dynamic(get_value/2),
	     assertz((set_value(Key,Value) :- recorded(Key,_,Ref),erase(Ref),recorda(Key,Value,_),!)),
	     assertz((set_value(Key,Value) :- recorda(Key,Value,_))),
	     assertz((get_value(Key,Value) :- recorded(Key,Value,_))).

rp_verbosity(0).
rp_version(0.42).
rp_tabfactors(6,0.00003).

:- dynamic rp_nogood_tabling/0.
:- dynamic subsumer_table/2.
% rp_nogood_tabling.

:- dynamic expanding/0.
:- dynamic rp_call_counting/0.

% comment next two lines to turn call counting off ...
% rp_call_counting.
% :- yap_flag(call_counting,on).

init :-
	rp_version(V),
	%format('[ RichProlog2 version ~p ]~n',[V]),
	rp_verbosity(Verb),
	%format('[ RichProlog - using verbosity level ~p ]~n',[Verb]),
	% initialise evidential predicate store
	%profile_reset,
	bb_put(obs_tree,[]).

preinit :- 
	init_obs.

init_obs :-
	bb_put(obs_tree,NT),
	io1(NT).

% :- prolog_type(Type), init(Type), init.

/* REMOVE THIS LINE FOR SWI */
%:- attribute(richprolog_exist/1).

%:- set_value(rp_op_count,0).

%rp_max_table_size(2000).
%scale_factor(1).

%
% size of table = alpha * e^(beta x) 
% - x is the number of hypotheses tested.
%


rp_max_table_size(N) :-
	get_value(rp_op_count,X),
	rp_tabfactors(Alpha,Beta),
	NN is integer(ceiling(Alpha * exp(Beta * X))),
	if(NN < 120, NN = N, N = 300) .

inc_op_count :- 
	get_value(rp_op_count,X),
	XX is X + 1,
	set_value(rp_op_count,XX).

tests_to_perform(X) :-
	rp_max_table_size(N),
	if(N < 50, X=50,
	if(N < 200, X=N, X=200)).

% format_i meta-predicate
replaceformat(Verb,F,format(A,L)) :-
	\+ var(F),
	functor(F,format_i,3),
	F =.. [_,N,A,L],
	N =< Verb,
	!.
replaceformat(Verb,F,true) :-
	\+ var(F),
	functor(F,format_i,3),
	F =.. [_,N,_,_],
	N > Verb,
	!.
replaceformat(_,X,X).

user:term_expansion((H :- R),(H :- NR)) :-
	rp_verbosity(N),
	mapnodes(replaceformat(N),R,NR).

% debugger macro
rpdb :-
	spy(attempt_sigma_1),
	% spy user:goal_expansion,
	spy(execquery),
	spy(replace_refutable).
/*
:- op(1175,xfx,'-:-'). % query macros

:- op(975,xfy,':::'). % attach quantifier to formula - below ','

:- op(970,xfy,'=>').

% don't need to redefine '-'

:- op(900,fx,rnot).

:- op(100,fx,'`'). 

%
% *** QUERY MACROS ***
%  ( see also '-:-' term_expansion below)
%

:- bb_put(query_macro_defs,[]).

*/

freevars(AP,BP,DiffVars) :-
	sumnodes(vars,AP,[],AVars),
	sumnodes(vars,BP,[],BVars),
	difference(BVars,AVars,DiffVars).

univquant([X],(forall - X)).

univquant([X|Y],(forall - X ::: NY)) :-
	univquant(Y,NY).

vars(X,Y,[X|Y]) :- term_frozen_var(X),!.
vars(_,Y,Y).

%
% *** EVIDENTIAL PREDICATE HANDLER *** 
%  (see also "'" term_expansion at bottom)
%

theoretical(X) :-
	\+ evidential(X),
	\+ var(X),
	non_connective(X).

evidential(X) :-
	\+ var(X),
	functor(X,H,_),
	(atom_concat('$evidence_', _, H) ;
         atom_concat('$neg_evidence_',_ , H)).

evidential(` X) :- callable(X).

evidential(rnot ` X) :- callable(X).

rewrite_evidential_predicate(P,NP,NNP) :-
	nonvar(P),
	P =.. [Funct|Args],
	atom_concat('$evidence_',Funct,NewFunct),
	atom_concat('$neg_evidence_',Funct,NegNewFunct),
	NP =.. [NewFunct|Args],
	NNP =.. [NegNewFunct|Args].

record_evidential_predicate(P,State) :-
	functor(P,Funct,Len),
	% keep an evidential predicate database
	bb_get(obs_tree,OT),
	(\+ member(Funct/Len/State,OT) ->
	  bb_put(obs_tree,[Funct/Len/State|OT])
          ;
          true
        ).
	%

io1([]).
io1(T) :-
	select(Funct/Len/State,T,NT0),
	otherstate(State,OtherState),
	select(Funct/Len/OtherState,NT0,NT),
	!,
	io1(NT).

io1(T) :-
	select(Funct/Len/_,T,NT),
	!,
	atom_concat('$evidence_',Funct,NewFunct),
	atom_concat('$neg_evidence_',Funct,NegNewFunct),
	length(Vars,Len),
	NP =.. [NewFunct|Vars],
	NNP =.. [NegNewFunct|Vars],
	assertz((user:NNP :- \+ user:NP)),
	io1(NT).

otherstate(positive,negative).
otherstate(negative,positive).

%
% *** QUERY REWRITER ***
%

rewrite_query(X,X) :-
	X \= (_ ::: _).	

% XXX - note second argument is for module - not yet implemented

rewrite_query((_ ::: _),_,_,_,_,_,_) :-
        %format('HERE !!!\n',[]),
        fail.

rewrite_query((Quant ::: Formula),  _, richprolog:query(Exist,Univ,NonRef, Exec,user),
	       Strict,Name0,Name,Exist) :-
        %format('HERE~n',[]),
	term_freeze(((Quant ::: Formula),Name0),(F1,Name1)),

	rewrite_query_frozen(F1,_,richprolog:query(Exist4,Univ3,NonRef0,Exec0,_),Strict,ExistTypes0,Found0),

	term_thaw((NonRef0,Exec0,Name1,Exist4,ExistTypes0,Univ3,Found0),
                  (NonRef,Exec,Name,Exist,ExistTypes,Univ,Found)),
	% apply the types to the variables in the new formula
	applytypes(ExistTypes),
	length(Found,FL), length(Exist,EL),
	((Strict == yes,FL =\= EL) ->
	    rp_syntax_error('Syntax error in query',(Quant:::Formula));
	    true),
	type_variables(Exist,Found),
	% check that there's no uninstantiated existential variables if appropriate
	((Strict == yes,missing_variables(Found)) ->
	    rp_syntax_error('No existentially quantified variables in positive parts',(Quant:::Formula));
	    true).


rewrite_query_frozen(Formula,_,richprolog:query(Exist,Univ,NonRef, Exec,user),Strict,ExistTypes,Found) :-
	% put into Sigma_2 and strip the variables
	prenex_frozen(Formula,F2),
	rewrite_query1(F2,Exist0,Univ,Matrix0),
	% pull out the types
	extract_types_from_term(Exist0,Exist1,ExistTypes),
	term_constructions(ExistTypes,ExistTC),
	clause_list(Matrix0,Matrix1),	
	extract_types(Matrix1,Matrix2),	
	(ExistTypes == [] ->
	    clause_list(Matrix3,Matrix2);
	    clause_list(Matrix3,[ExistTC|Matrix2])),
	(Strict == yes ->
	    Exist1 = Exist;
	    additional_existential_frozen(Exist1,Univ,Matrix3,Exist)),
	% rewrite into positive and negative parts of the query; also remove => syntax, etc ...
	replace_refutable(Exist,Univ,toplevel,Matrix3,NonRef ,Exec,ExistTypes,Found),
	glist(Found).


glist(X) :- var(X),X=[].
glist(X) :- \+ var(X), X = [_|R],glist(R).
glist(X) :- X == [].

rewrite_query1((exists - X ::: Rest),Exist,Univ,Matrix) :-
	!,
	rewrite_query1(Rest,Exist0,Univ,Matrix),
	lv1(X,EH),
	append(EH,Exist0,Exist).

rewrite_query1((forall - X ::: Rest),[],Univ,Matrix) :-
	!,
	rewrite_query1(Rest,[],Univ0,Matrix),
	lv1(X,UH),
	append(UH,Univ0,Univ).

rewrite_query1(Query,[],[],Query) :- Query \= (_ ::: _).

additional_existential_frozen(Exist0,Univ,Matrix,Exist) :-
	term_variables_frozen(Matrix,Vars),
	var_union_frozen(ETemp,Univ,Vars),
	var_union_frozen(EH,Exist0,ETemp),
	append(EH,Exist0,Exist). % note this means that Exist == ETemp ch. so.


additional_existential(richprolog:query(Exist0,Univ,Matrix,Module,S),
	              richprolog:query(Exist,Univ,Matrix,Module,S)) :-
	term_variables(Matrix,Vars),
	var_union(ETemp,Univ,Vars),
	var_union(EH,Exist0,ETemp),
	append(EH,Exist0,Exist). % note this means that Exist == ETemp ch. so.

lv1(U0,[U0]) :- term_frozen_var(U0),!.
lv1('@'(U0,T),['@'(U0,T)]) :- term_frozen_var(U0),!. % XXX - to be removed when we sep out types
lv1([H|R],[H|R]).


%
% prenex_subst(F1,F2) - formula F2 is F1 in prenex normal form, with query macro
%  substitutions made
%

%
% Use of cuts here is to ensure a unique solution; much easier than full logical specification.
%
prenex_frozen(((Quant ::: F1) ; F2), (Quant ::: (NewF))) :-
	!,
	variable(Quant,Variable),
	rename_variables(Variable,F2,NF2),
	prenex_frozen((F1;NF2),NewF).

prenex_frozen(((Quant ::: F1) , F2), (Quant ::: (NewF))) :-
	!,
	variable(Quant,Variable),
	rename_variables(Variable,F2,NF2),
	prenex_frozen((F1,NF2),NewF).

prenex_frozen((F1 ; (Quant ::: F2)), (Quant ::: (NewF))) :-
	!,
	variable(Quant,Variable),
	rename_variables(Variable,F1,NF1),
	prenex_frozen((NF1;F2),NewF).

prenex_frozen((F1 , (Quant ::: F2)), (Quant ::: (NewF))) :-
	!,
	variable(Quant,Variable),
	rename_variables(Variable,F1,NF1),
	prenex_frozen((NF1,F2),NewF).

prenex_frozen((F1,F2),F) :-
	prenex_frozen(F1,F1P),
	prenex_frozen(F2,F2P),
	more_prenex_possible((F1P,F2P)),
	!,
	prenex_frozen((F1P,F2P),F).

prenex_frozen((F1,F2),(F1P,F2P)) :-
	prenex_frozen(F1,F1P),
	prenex_frozen(F2,F2P).

prenex_frozen((F1;F2),F) :-
	prenex_frozen(F1,F1P),
	prenex_frozen(F2,F2P),
	more_prenex_possible((F1P;F2P)),
	!,
	prenex_frozen((F1P;F2P),F).

prenex_frozen((F1;F2),(F1P;F2P)) :-
	prenex_frozen(F1,F1P),
	prenex_frozen(F2,F2P).

prenex_frozen((rnot (Quant:::Formula)),( NQuant :::(rnot NFormula))) :-
	!,
	opposite_quantifier(Quant,NQuant),
	prenex_frozen(Formula,NFormula).

prenex_frozen((rnot Formula),( rnot NFormula)) :-
	prenex_frozen(Formula,NFormula).

prenex_frozen((F1 => F2), NewF) :-
	!,
	prenex_frozen(((rnot F1);F2),NewF).

prenex_frozen((Q ::: Formula),(Q:::NewFormula)) :-
	!,
	prenex_frozen(Formula,NewFormula).

prenex_frozen(Formula,NFormula) :-
	non_connective(Formula),
	bb_get(query_macro_defs,Defs),
	term_thaw(Formula,TF),
	query_macro_member(Defs,TF,Subst),
	!,
	prenex_frozen(Subst,NFormula).

prenex_frozen(F,F) :-
	non_connective(F).

query_macro_member([query_macro(F1,S1)|_],F2,S2) :-
	term_thaw(query_macro(F1,S1),query_macro(F2,S2)), 
	!.

query_macro_member([_|R],F,S) :-
	query_macro_member(R,F,S).

more_prenex_possible(((_:::_),_)).
more_prenex_possible(((_:::_);_)).
more_prenex_possible((_,(_:::_))).
more_prenex_possible((_;(_:::_))).

opposite_quantifier(exists-X,forall-X).
opposite_quantifier(forall-X,exists-X).

variable(_-X,X).

new_variable(X) :-
	term_freeze(_,X).

rename_variables(Variable,F,NF) :-
	new_variable(NewVariable),
	mapnodes(replace(Variable,NewVariable),F,NF).

%
% Creates the construct_term predicte for the Sigma_1 query if necessary
%

term_constructions(VarTypes,construct_term_list(Types,Vars,Depth)) :-
	richprolog:fixeddepth(Depth),
	tc1(VarTypes,Types,Vars).
term_constructions(VarTypes,construct_term_list(Types,Vars)) :-
	\+ richprolog:fixeddepth(_),
	tc1(VarTypes,Types,Vars).

tc1([],[],[]).
tc1(['@'(Var,Type)|R],['@'(Type)|TR],[Var|VR]) :-
	tc1(R,TR,VR).

replace_refutable(Exist,Univ,Restrict,(X,Y),Conj ,Disj,ExistTypes,Found) :- 
	replace_refutable(Exist,Univ,Restrict,X,MX,NX,ExistTypes,Found),
	replace_refutable(Exist,Univ,Restrict,Y,MY,NY,ExistTypes,Found),
	form_conj_disj(MX,MY, Conj, _),
	form_conj_disj(NX,NY, _, Disj).

replace_refutable(Exist,Univ,Restrict,(X;Y), Disj , Conj,ExistTypes,Found) :- 
	replace_refutable(Exist,Univ,Restrict,X,MX,NX,ExistTypes,Found),
	replace_refutable(Exist,Univ,Restrict,Y,MY,NY,ExistTypes,Found),
	form_conj_disj(MX,MY, _, Disj),
	form_conj_disj(NX,NY, Conj, _).

replace_refutable(Exist,Univ,toplevel,rnot(X), true, MX,_,_) :-
	%\+ evidential(X),
	replace_refutable(Exist,Univ,refutable,X,MX,_,_,_).

% separate cases for theoretical and evidential to allow easy modification
replace_refutable(E, U, toplevel, X, X, fail,ExistTypes, Found) :-
	non_connective(X),
	evidential(X),
	(args_in_set(X,U),\+ ground(X) -> 
	   rp_syntax_error('Universal variables used in non-refuted clause',X);
	\+ all_in_set(X,E,U) ->
	   rp_syntax_error('Unbound variable used',X);
	   true),
	exists_in_set(X,ExistTypes,Found).

replace_refutable(E, U, toplevel, X, X, fail, ExistTypes,Found) :-
	non_connective(X),
	theoretical(X),
	(args_in_set(X,U),\+ ground(X)  -> 
	   rp_syntax_error('Universal variables used in non-refuted clause',X);
	\+ all_in_set(X,E,U) ->
	   rp_syntax_error('Unbound variable used',X);
	   true),
         exists_in_set(X,ExistTypes,Found).

%replace_refutable(E,U,refutable,X,X,\+ X, _) :-
replace_refutable(E,U,refutable,X,X,fail, _,_) :-
	(non_connective(X); evidential(X)),
	(\+ all_in_set(X,E,U) ->
	    rp_syntax_error('Unbound variable used',X);
	    true).

% A micro propositional solver; given A and B find A and B, A or B
form_conj_disj(true, true, true, true) :- !.
form_conj_disj(true, X, X, true) :- !.
form_conj_disj(X, true, X, true) :- !.
form_conj_disj(fail, fail, fail, fail) :- !.
form_conj_disj(fail, X, fail, X) :- !.
form_conj_disj(X, fail, fail, X) :- !.
form_conj_disj(X, Y, (X,Y),(X;Y)). 

%
% *** QUERY ENGINE ***
%

query_reset :-
	reset_depth,
	reset_nogoods,
	% rp_count_reset, -- needed for "whole-query" counting
	!.

query(Exist,Univ,NonRefMatrix,ExecMatrix,Module) :-
	install_rp_signal,
	query_reset,
	(rp_nogood_tabling -> apply_atts(Exist,[+(richprolog_exist(Exist))]); true),
	!,
	catch(query1(Exist,Univ,NonRefMatrix,ExecMatrix,Module) ,
	      richprolog_no_solution_failure,
	      (uninstall_rp_signal,!,fail)),
	format('finished query1~n',[]),
	uninstall_rp_signal.

set_rp_deductive_phase :- 
	eraseall(rp_ded_ind),
	recorda(rp_ded_ind,deductive,_).
	
set_rp_inductive_phase :- 
	eraseall(rp_ded_ind),
	recorda(rp_ded_ind,inductive,_).

set_rp_inductive_phase :-
	set_rp_deductive_phase,
	fail.

rp_inductive_phase :- recorded(rp_ded_ind,inductive,_).
rp_deductive_phase :- recorded(rp_ded_ind,deductive,_).

query1(Exist,Univ,NonRefMatrix, ExecMatrix,Module) :-
        format_i(3,'[ Attempting initial \\Sigma_1 query: ~p]~n',[NonRefMatrix]),
	(
         catch(
	    (set_rp_deductive_phase,Module:NonRefMatrix),
	    E,
	    (format_i(0,'[ Exception in \\Sigma_1 sub-query: ~p ]~n',[NonRefMatrix]),
		       print_message(error,E),
		       throw(E))
              ),
	set_rp_inductive_phase,
	attempt_sigma_1(Exist,Univ,ExecMatrix,Module)
 	;
 	!,
 	format('attempt_sigma_1 failed',[]),
 	fail).

p.

attempt_sigma_1(Exist,Univ,ExecMatrix,Module) :-
	format_i(3,'[ Attempting negation of \\Sigma_1 query: ~p ]~n',[ExecMatrix]),
	format_i(2,'[ Att neg vars: ~p ]~n',[Exist]),
	inc_op_count,
	(recorded(richprolog_reattempt_query,true,Ref) 
        ->
	    erase(Ref),
	    throw(richprolog_new_data_reattempt_query)
	;
	    true),
	((catch(
	    (
	    % DEBUG HOOK
	    %format("Exist is ~p~n",[Exist]),
	    (Exist == [disj([conj([adjrel(1,6)],[])])] -> halt; true),
	    rp_count_reset,
	    as1(Module,ExecMatrix)),
	    E,
	    ( format_i(0,'Exception in \\Sigma_1 sub-query: ~p~n',[ExecMatrix]),
	    print_message(error,E),
	    throw(E))))
        -> 
	    record_count(Exist,final),
	    record_failure(Exist),
	    % rp_count_reset, -- for "whole-query" counting
            fail
        ;  % - backtrack to another solution of the initial query
	    format_i(4,'[ Success! result ~p ~p~n ]',[ Exist, Univ]),
	    RPLastResult = Exist,
	    bb_put(rplr, RPLastResult)
	). 

as1(Module,ExecMatrix) :-
	catch(
	    (Module:ExecMatrix),  % <- negation of Matrix is called here; note ExecMatrix is already negated ...
	    rp_nogood_bailout,
	    (format('catching exception~n',[]),set_rp_deductive_phase)).

record_failure(_) :- \+ rp_nogood_tabling,!.

% note recordzifnot can't be used as it doesn't check for subsumption.
record_failure(NExist) :-
	key_statistics(rp_exist_fails,N,_,_),
	rp_max_table_size(Max),
	(N < Max; Max == 0), % use Max = 0 for unlimited table size
	format_i(2,'*** RECORD FAILURE: ADDING NOGOOD *** ~p *** TABLE SIZE ~p *** MAX SIZE ~p ****~n',[NExist,N,Max]),
	recordz(rp_exist_fails,NExist,_),%;true),
	subsumer_table(FTable,RTable),
	add_term(NExist,FTable),
	add_term(NExist,RTable),
	!.

record_failure(NExist) :-
	format_i(4,'*** RECORD FAILURE: MAX NOGOOD TABLE SIZE REACHED *** ~p ***~n',[NExist]),
	recordz(rp_exist_fails,NExist,_),
	subsumer_table(FTable,RTable),
	add_term(NExist,FTable),
	add_term(NExist,RTable),
	find_minimal_pair(TS,RTable),
	delete_subsumed(FTable,RTable,TS),
	add_term(TS,FTable),
	add_term(TS,RTable),
	recordz(rp_exist_fails,TS,_),
	format_i(4,'*** TABLE EXPANDED - GENERALIZING TO ~p***~n',[TS]).

record_failure :- 
	format('record_failure is bugged ~n',[]),
	trace.

record_count(_,_) :- \+ rp_call_counting,!.

record_count(E,Loc) :-
	call_count_data(A,B,C),
	user:similar_check(F),
	subterm_count(E,F,N),
	format('&&&&& ~p &&&&& ~p & ~p & ~p &&&&& ~p &&&&& ~p~n',[E,A,B,C,N,Loc]).

rp_count_reset :- \+ rp_call_counting,!.

rp_count_reset :-
	call_count_reset.

find_minimal_pair(TS,BTable) :-
	recorda(rp_mincount,rpm(_,_,_,40000000),_), % bignum
	tests_to_perform(Max),
	set_value(goo,0),
	repeat,
	fmp1(Max,BTable),
	!,
	recorded(rp_mincount,rpm(_,_,TS,_),Ref),
	erase(Ref).

fmp1(Max,BTable) :-
	get_value(goo,Tries),
	Tries < Max,
	NTries is Tries + 1,
	set_value(goo,NTries),
	random_element(Elem1),
	random_element(Elem2),
	recorded(rp_mincount,rpm(_,_,_,MinimalCount),Ref),
	\+ variant(Elem1,Elem2),
	term_subsumer(Elem1,Elem2,TS),
	term_subsumes_count(TS,BTable,N),
	(N < MinimalCount ->
	    erase(Ref),
	    recorda(rp_mincount,rpm(Elem1,Elem2,TS,N),_),
	    fail
	;
	    fail).

fmp1(Max,_) :- 
	get_value(goo,Tries),
	Tries >= Max.

term_sub_count(TS,N) :-
	compile_term(forward,TS,TSTab),
	initial_segment(TS,Seg),
	set_value(tsc,0),
	repeat,
	tsc1(TSTab,Seg),
	!,
	delete_subsumer_table(TSTab),
	get_value(tsc,N).

tsc1(Tab,Seg) :-
	recorded(rp_exist_fails,Seg,_),
	term_subsumes(Seg,Tab),
	get_value(tsc,N),
	NN is N + 1,
	set_value(tsc,NN),
	fail.

tsc1(_,_).


random_element(Elem) :-
	key_statistics(rp_exist_fails,T,_,_),
	TableSize is T + 1,
	random(1,TableSize,Num),
	%format('Looking up ~p th instance~n',[Num]),
	nth_instance(rp_exist_fails,Num,Ref),
	recorded(rp_exist_fails,Elem,Ref).

% workaround ...
/*
random_element(Elem) :-
	key_statistics(rp_exist_fails,T,_,_),
	TableSize is T + 1,
	random(1,TableSize,Num),
	nth_instance_workaround(rp_exist_fails,Elem,Num).
*/

nth_instance_workaround(DBRef,Elem,Num) :-
	set_value(blah,Num),
	eraseall(foofoo),
	repeat,
	ni1(DBRef),
	!,
	recorded(foofoo,Elem,_).

ni1(DBRef) :-
	recorded(DBRef,Elem,_),
	get_value(blah,Num),
	Num > 0,
	NN is Num - 1,
	set_value(blah,NN),
	eraseall(foofoo),
	recorda(foofoo,Elem,_),
	fail.

ni1(_) :-
	get_value(blah,Num),
	Num =< 0.

delete_subsumed(FT,BT,TS) :-
	empty_subsumer_table(forward,TSTable),
	add_term(TS,TSTable),
	repeat,
	ds1(TSTable,FT,BT),
	!,
	delete_subsumer_table(TSTable).

ds1(TSTable,FT,BT) :-
	recorded(rp_exist_fails,Elem,Ref),
	(term_subsumes(Elem,TSTable) ->
	    erase(Ref),
	    delete_term(Elem,FT),
	    delete_term(Elem,BT),
	    fail
	;
	    fail).

ds1(_,_,_).


%
% - Check for a failure
% - if attributed, add attributes to variables in unified value.
%
verify_attributes(Var,_,[]) :-
	record_count(_,verify_atts_start),
	rp_nogood_tabling,
	get_atts(Var,[+(richprolog_exist(ExistVars))]),
	record_count(_,now_have_atts),
	fail,
	check_sub_fail(ExistVars), 
	!,
	%format('*** NOGOOD BAILOUT *** ~p ~p ~p ***~n',[Var,Val,ExistVars]),
	%Goals = [term_variables(Val,ValVars), 
	%        apply_atts(ValVars,[+(richprolog_exist(ExistVars))])],
	%Var = Val,
	(rp_deductive_phase -> !,inc_op_count,fail; (throw(rp_nogood_bailout))).

verify_attributes(Var,Val,[term_variables(Val,ValVars),
        apply_atts(ValVars,[+(richprolog_exist(ExistVars))]),Var = Val]) :-
	format('Val is ~p~n',[Val]),
	rp_nogood_tabling,
	get_atts(Var,[+(richprolog_exist(ExistVars))]), 
	!.

xxxhook :- format('debug hook~n',[]).
%verify_attributes(X,Y,[]).

%apply_atts(_,_) :- !.

apply_atts([],_).
apply_atts([V|R],ExistVars) :-
	put_atts(V,ExistVars),
	apply_atts(R,ExistVars).



%check_sub_fail(_) :- fail.
% this is now coded in C - see subsumer module for details
check_sub_fail(ExistVars) :-
	%format('*** TESTING FOR NOGOOD BAILOUT *** ~p ***~n',[ExistVars]),
 	subsumer_table(FT,_),
        term_subsumes(ExistVars,FT),
	!.

%check_sub_fail(_).

% next bit for debugging
print_fail_set :-
	key_statistics(rp_exist_fails,N,_,_),
	format(' *** CURRENT NOGOODS - TABLE SIZE ~p *** ~n',[N]),
	repeat,
	pfs1,
	!.

/*temp debug version */
/*
reset_nogoods :- 
	eraseall(rp_exist_fails),
	eraseall(rp_univ_fails),
	recorda(rp_tabled_entries,0,_),
	asserta(subsumer_table(FTP,RTP)).

*/

reset_nogoods :-
	\+ rp_nogood_tabling,!.

reset_nogoods :-
	!,
	eraseall(rp_exist_fails),
	eraseall(rp_univ_fails),
	(subsumer_table(FT,RT) -> delete_subsumer_table(FT),
	                          delete_subsumer_table(RT),
	                          retractall(subsumer_table/2)
           ; true),
	empty_subsumer_table(forward,FTP),
	empty_subsumer_table(backward,RTP),
	eraseall(rp_tabled_entries),
	recorda(rp_tabled_entries,0,_),
	asserta(subsumer_table(FTP,RTP)).

% for debugging ...
pfs1 :-
	recorded(rp_exist_fails,E,_),
	format('Nogood; Exist: ~p ~n',[E]),
	fail.

pfs1 :- recorded(rp_ts_data,T,_),
	format('Subsumer Table; ~p~n',[T]),
	fail.

pfs1.

% from Yap sources ...
name_string(I,L,[C|L]) :- I < 26, !, C is I+65.
name_string(I,L0,LF) :-
	I1 is I mod 26,
	I2 is I // 26,
	C is I1+65,
	name_string(I2,[C|L0],LF).

rp_last_result(X) :- bb_get(rplr, X).
%
% For adding more data to the database
%
% XXX - negated data is not removed correctly; suppose the
%  user/programmer adds data inconsitent with what's there -
%  this is outside the richprolog semantics

% this is called from the 'another_handler' below.  It adds the new 
% evidence to the database, succeeds when done, fails otherwise.

% XXX - fix hard coded modules in here
add_data(Other) :-
	(current_predicate(user:rp_evidence/1) ->
	    user:rp_evidence(Other);
	    true),
	((user:term_expansion(Other, ONN),evidential(Other))  ->
	    assertz(user:ONN);
	    assertz(user:Other)),
	format_i(3,'[ Added data: ~p]~n',Other), 
	(found_evidence_in_program -> recordaifnot(richprolog_reattempt_query,true,_), true). 
	% if no evidence, this will get a fail after add_data called

stream_setup :-	
	current_predicate(user:rp_data_init/1),
	user:rp_data_init(Out),
	recorda(richprolog_stream_data,Out,_),
	format('setup succeeded~n',[]).
stream_setup :- 
	\+ current_predicate(user:rp_data_init/1).

add_data_from_stream :-	
	current_predicate(user:rp_data_next/3),
	format_i(3,'[ Adding data from stream 1 ]\n',[]),
	recorded(richprolog_stream_data,In,Ref),
	format_i(3,'[ Adding data from stream 2 ]\n',[]),
	erase(Ref),
	(user:rp_data_next(In,Out,Predicates) ->
	    true;
	    format('ERROR IN RP_DATA_NEXT handler',[])),
	add_data_all(Predicates),
	recorda(richprolog_stream_data,Out,_),
	format_i(3,'[ Adding data from stream 3 ]\n',[]).

add_data_from_stream :-
	\+ current_predicate(user:rp_data_next/3),
	format('[ Error: adding new stream data when rp_data_next not defined ]\n',[]).

add_data_all([]).
add_data_all([H|R]) :- add_data(H),add_data_all(R).

stream_cleanup:-
	format('Stream cleanup~n',[]),
	current_predicate(user:rp_data_cleanup/1),
	recorded(richprolog_stream_data,Out,Ref),
	user:rp_data_cleanup(Out),
	erase(Ref).

stream_cleanup :- 
	\+ current_predicate(user:rp_data_cleanup/1).
    
%
% *** MISC PREDICATES ***
%

difference(BVars,AVars,DiffVars) :-
	sort(BVars,SB),
	sort(AVars,SA),
	diff1(SB,SA,DiffVars).
	
diff1([],_,[]).

diff1(X,[],X).

diff1([BV|BR],[AV|AR],[BV|DR]) :-
	BV @< AV,
	diff1(BR,[AV|AR],DR).

diff1([BV|BR],[AV|AR],Diff) :-
	BV @> AV,
	diff1([BV|BR],AR,Diff).

diff1([AV|BR],[AV|AR],Diff) :-
	diff1(BR,[AV|AR],Diff).

replace(Comp,Atom,Comp,Atom).
replace(Comp,_,Comp2,Comp2) :- Comp \= Comp2.

clause_list((A,B) , [A,B]) :-
	\+ functor(A,':-',_),
	\+ functor(B,',',_).

clause_list((A,B) , [A|NB]) :-
	\+ functor(A,':-',_),
	clause_list(B,NB),
	functor(B,',',_).

clause_list(A , [A]) :-
	\+ functor(A,',',_),
	\+ functor(A,':-',_).

disj_list(A,[A]) :-
	\+ functor(A,';',_).

disj_list((A;B),[A,B]) :-
	\+ functor(B,';',_).

disj_list((A;B),[A|NB]) :-
	disj_list(B,NB),
	functor(B,';',_).

copy_term_workaround(In, Out) :-
        recorda(copier, In, Ref),
        recorded(copier, Out, Ref),
        erase(Ref).

non_connective(X) :-
	%X \= (onot _),
	X \= (rnot _),
	X \= (_ , _),
	X \= (_ ; _),
	X \= (_ | _),
	% X \= (_ & _),
	X \= (_ => _).
	%X \= (_ ::: _ ).

% applies a type to the variables in a query
type_variables([],[]).
type_variables([X|R],[X-T|NR]) :-
	rp2_type:check_type(T,X),
	!,
	type_variables(R,NR).
type_variables([X|R],[X-_|NR]) :-
	type_variables(R,NR).


%
% variable member predicates - for frozen variables
%

all_in_set(T,V1,V2) :-
	append(V1,V2,V3),
	args_in_set(T,V3).

exists_in_set(T,ET,Found) :-
	term_variables_frozen(T,TermVars),
	o_in_set(TermVars,ET,Found).

missing_variables([_-T|R]) :-
	\+ ground(T);
	missing_variables(R).

args_in_set(Term,VarList) :-
	term_variables_frozen(Term,TermVars),
	args_in_set1(TermVars,VarList).

args_in_set1([],_).
args_in_set1([Arg|Rest], Set) :-
	member(Arg,Set),
	args_in_set1(Rest,Set).


% XXX - inefficent, but will be ok for small nos of variables.
o_in_set([],_,_).

o_in_set([V0|R],ET,[V0-'@'(T)|NR]) :-
	member('@'(V0,T),ET),
	o_in_set(R,ET,NR).

o_in_set([V0|R],ET,[V0-found|NR]) :-
	\+ member('@'(V0,_),ET),
	o_in_set(R,ET,NR).

o_in_set([V0|TR],ET,[V1-T1|VR]) :-
	V0 \= V1,
	(o_in_set([V0|TR],ET,VR)
    ;
	o_in_set(TR,ET,[V1-T1|VR])).



%
% write/debug - these need a macro varsion and a dynamically changeable version
%

%format_i(Level,T1,T2) :-
%	rp_verbosity(IL), 
%	!,
%	if(Level =< IL, format(T1,T2), true).

non_vars([H|R1],R2) :-
	\+ var(H),
	non_vars(R1,R2).

non_vars([H|R1],[H|R2]) :-
	var(H),
	non_vars(R1,R2).

non_vars([],[]).



%
% *** FREEZE/THAW ***
%

term_freeze(Term,FTerm,Variables) :-
	term_freeze(Term,FTerm,Variables,0). 

term_freeze(Term,FTerm,Variables, Base) :-
	term_variables(Term,Variables),
	copy_term(Term,FTerm),
	term_variables(FTerm,NTV),
	assign_variables(NTV,Base).

term_thaw(FTerm,TTerm,Variables) :-
	mapnodes(replace_variable(Variables),FTerm,TTerm).

%
% freeze/thaw without explicit variable lists - note this does not garbage 
%  collect, so will pop stacks if not used judiciously.  Also woefully 
%  inefficient, etc.  I just use it once per query, so should be ok.
%

:- bb_put(freeze_list,[]).

term_freeze(Term,FTerm) :-
	bb_get(freeze_list,FL),
	length(FL,Len),
	term_freeze(Term,FTerm,Variables,Len),
	append(FL,Variables,NFL),
	bb_put(freeze_list,NFL).

term_thaw(FTerm,TTerm) :-
	bb_get(freeze_list,FL),
	term_thaw(FTerm,TTerm,FL).

assign_variables([],_).

assign_variables(['$Var'(X)|Rest],X) :-
	NX is X + 1,
	assign_variables(Rest,NX).

replace_variable(_,N,N) :- N \= '$Var'(_).

replace_variable(Variables,'$Var'(X),V) :-
	nth0(X,Variables,V).

term_frozen_var('$Var'(X)) :- integer(X).

term_variables_frozen(Term,Vars) :-
	sumnodes(fva,Term,[],Vars0),
	sort(Vars0,Vars1),
	uniq(Vars1,Vars).

fva(X,Y,[X|Y]) :- term_frozen_var(X),!.
fva(_,X,X).

uniq([X],[X]).
uniq([],[]).
uniq([X,X|R1],[X|R2]) :- uniq(R1,R2).
uniq([X,Y|R1],[X,Y|R2]) :- X \== Y,uniq(R1,R2).


%
% *** SIGNAL HANDLING ***
%   gone for now ...
install_rp_signal :- !.
install_rp_signal :-
	on_signal(sig_usr1,OldSH,rp_handle_signal),
	bb_put(oldsh,OldSH).

% XXX - I have no idea why this last cut is needed; maybe
%  without it we're repeatedly backtracking through this,
%  making a new choice point every time.
uninstall_rp_signal :- !.
uninstall_rp_signal :-
	get_value(oldsh,OldSH),
	bb_get(sig_usr1,_,OldSH),!.

rp_handle_signal :-
	write('Interrupt received; aborting query\n'),
	throw(richprolog_no_solution_failure).

rp_syntax_error(Message,BadSyntax) :-
	rp_error( syntax_error(BadSyntax,0,Message,[],0,0)).

%rp_error(X) :- throw(X).
rp_error(X) :- do_error(X,'mess').

do_error(Type,Message) :-
        throw(error(Type,Message)).


%
% *** EXPANSION MACROS ***
%
/*
richprolog:term_expansion(A,B) :- user:term_expansion(A,B).

user:term_expansion((A -:- B), '$null') :-
	A \= (_,_),
	term_freeze(query_macro(A,B),query_macro(AP,BP)),
	freevars(AP,BP,FreeVars),
	univquant(FreeVars,UFV),
	bb_get(query_macro_defs,Defs),
	\+ member(query_macro(AP,_),Defs),
	bb_set(query_macro_defs,[query_macro(AP,(UFV ::: BP))|Defs]),
	!,
	fail.

user:term_expansion(end_of_file,end_of_file) :- !.
*/
rewrite_evidential_body(OC,NC,Style) :-
	mapnodes(evidential_rewrite(Style),OC,NC).

evidential_rewrite(_,X,X) :- var(X),!.

evidential_rewrite(B,`X,Y) :-
	evidential(`X),
	!,
	(B == fact -> record_evidential_predicate(X,positive); true),
	(B == body -> evidence_in_program_found ; true),
	rewrite_evidential_predicate(X,Y,_).

evidential_rewrite(B,rnot ` X,Y) :-
	evidential(rnot ` X),
	!,
	(B == fact -> record_evidential_predicate(X,negative); true),
	(B == body -> evidence_in_program_found ; true),
	rewrite_evidential_predicate(X,_,Y).

evidential_rewrite(_,X,X).

evidence_in_program_found :- 
	\+ found_evidence_in_program,
	!,
	format_i(1,'[ Found evidential predicate in program body - no optimized queries ]~n',[]),
	asserta(found_evidence_in_program).

evidence_in_program_found.

rewrite_sigma2_body(OC,NC) :-
	mapnodes(forall_rewrite,OC,NC).

forall_rewrite(X,X) :- term_frozen_var(X),!.

forall_rewrite((forall - U0 ::: C),Q0) :-
	!,
	rewrite_query_frozen((forall - U0 ::: C),user,Q0,no,_,_).

forall_rewrite(X,X) :-
	X \= (forall - _ ::: _).

syntax_term_expansion((H :- B), NC) :-
	( evidential(H) ->
	    rp_syntax_error('Use of evidential predicate in head of clause',(H :- B)); true),
	term_freeze((H :- B),Froz),
	rewrite_sigma2_body(Froz,NC0),
	rewrite_evidential_body(NC0,NC1,body),
	term_thaw(NC1,NC).

syntax_term_expansion_fact(X,NC) :-
	\+ functor(X,:-,2),
	evidential_rewrite(fact,X,NC).

% simple top level
%
%  This code is heavily based on the similar yap code.
%



tl :-
	preinit,
	repeat,
	prompt(_,'[rp] ?- '),
	catch(
	      read_term(RawQuery,[variable_names(VNames)]),
	      Err,
	      (format('Exception reading term ~p\n',[Err]),fail)),
	catch(execquery(RawQuery,VNames),
              Err,
	      (format('Exception processing query ~p\n',[Err]),fail)).

execquery(end_of_file,_) :-
	halt.
execquery(RawQuery,Names) :-
	RawQuery = (_ ::: _),
	!,
	execquery1(RawQuery,Names).

execquery(RawQuery0,Names) :-
	RawQuery0 \= (_ ::: _),
	yap_flag(typein_module,Mod),
	term_variables(RawQuery0,Vars),

	extract_types_from_term(RawQuery0,RawQuery1,Types),

	clause_list(RawQuery1,RawQuery1L),
	append(Types,RawQuery1L,RawQuery2L),
	clause_list(RawQuery2,RawQuery2L),
	rewrite_evidential_body(RawQuery2,RawQuery,query),
	call(Mod:RawQuery),
	report_result(Names,Vars),
	another_handler,
	!,
	fail.
	
execquery(_,_) :-
	format(user_error,'[rp] no~n',[]),
	fail.

%:- spy execquery.

execquery1(RawQuery0,Names0) :-
	rewrite_evidential_body(RawQuery0,RawQuery,query),
	rewrite_query(RawQuery,user,Query,yes,
	              Names0,Names,ReportVars),
	!, % XXX - there's a bug that's causing an unnecessary backtrack - don't know where but this
           % seems to fix it. 
	%statistics,
	stream_setup,
	repeat,
	catch((execquery2(Query,Names,ReportVars)),
	      richprolog_new_data_reattempt_query,
	      (eraseall(richprolog_reattempt_query),fail)).

execquery2(Query,Names,ReportVars) :-
	(call(Query),
	report_result(Names,ReportVars),
	another_handler,
	fail)
	;
	(format(user_error,'[rp] no~n',[]),
	prompt('[rp] ?- '),
	true).

query_adddata_catch(Exist,Univ,NonRefMatrix,ExecMatrix,Module) :-
	!,
	catch(query1(Exist,Univ,NonRefMatrix, ExecMatrix,Module),
	      richprolog_new_data_reattempt_query,
	      query1(Exist,Univ,NonRefMatrix, ExecMatrix,Module)).

another_handler :-
	prompt(_,'[rp] |:'),
	format('~n[rp] Enter more evidence (or ";", <return> or "help."): ',[]),
	peek_code(C),
	(C == 0'; ->  skip(10), fail
						% ' fix syntax highlighting ...
        ;
	C == 0'\\ ->  skip(10), add_data_from_stream
						% ' fix syntax highlighting ...
        ;

	C == 10 -> skip(10), format(user_error,"[rp] yes~n", [])
	;
	C == -1 -> halt
        ;
	  read_evidence
        ),
	!.

read_evidence :-
	read(EV),
	( another_response(EV) ->
	    fail
	;
	    another_handler
	).

another_response(help) :-
	write('In addition to failing/backtracking at this point, you\n'),
	write('may add new evidence at the prompt, ended with a period.\n'),
	write(' - ";" - backtrack to next goal with current evidence set\n'),
	write(' - "\" - call stream handler to get data from the stream\n'),
 	write(' - <return> - exit query\n'),
	write(' - "help." - this information\n'),
	write(' - <evidence>. - add evidence and reattempt query\n'),
	write('Valid formats for evidence are: \n'),
	listing(rp_evidence),
	fail.
another_response(none) :- !, fail.
another_response(quit) :-
	write('Exiting query at user request'),
	throw(richprolog_no_solution_failure).
another_response(Other) :-
	add_data(Other),
	fail.  % backtrack in optimized case

report_result(Names0,ReportVars) :-
	delete_nonreported(ReportVars,Names0,Names1),
	sort(Names1,Names2),
	unite_identical(Names2,Names3),
	delete_empty(Names3,Names),
	write_result(Names).

write_result([H=Val|R]) :-
	!,
	write_head(H),
	format(' = ~p~n',[Val]),
	write_result(R).
write_result([]).

write_head(A=B) :-
	!,
	write_head(A),
	format(' = ~p',[B]).
write_head(A) :-
	format('~p',[A]).

unite_identical([],[]).
unite_identical([H=V|R],[NV|NR]) :-
	unite_identical1(H=V,R,NR0,NV),
	unite_identical(NR0,NR).
unite_identical1(FV,[],[],FV).
unite_identical1(H=V,[HP=Val|R],NR,FV) :-
	V == Val,
	unite_identical1((H = HP) = V,R,NR,FV).
unite_identical1(H=V,[HP=Val|R],[HP=Val|NR],FV) :-
	V \== Val,
	unite_identical1(H = V,R,NR,FV).

delete_empty([],[]).
delete_empty([A=V|R],NR) :-
	var(V), atom(A),
	!,
	delete_empty(R,NR).
delete_empty([A=V|R],[A|NR]) :-
	var(V), \+ atom(A) ,
	!,
	delete_empty(R,NR).
delete_empty([A=V|R],[A=V|NR]) :-
	\+ var(V),
	!,
	delete_empty(R,NR).

delete_nonreported(Reported,A,B) :-
	selectlist(vmember(Reported),A,B).

vmember([H|_],_=Elem) :- Elem == H.
vmember([_|R],A=Elem) :- vmember(R,A=Elem).

var_union_frozen([],_,[]).
var_union_frozen([X|L1],L2,[X|L3]) :-
	\+ member(X,L2),
	var_union_frozen(L1,L2,L3).
var_union_frozen(L1,L2,[X|L3]) :-
	member(X,L2),
	var_union_frozen(L1,L2,L3).


var_union([],_,[]).
var_union([X|L1],L2,[X|L3]) :-
	\+ vu_mem(X,L2),
	var_union(L1,L2,L3).
var_union(L1,L2,[X|L3]) :-
	vu_mem(X,L2),
	var_union(L1,L2,L3).

vu_mem(X,[H|_]) :- X == H.
vu_mem(X,[_|R]) :- vu_mem(X,R).

% prolog term subsumer, like the sicstus operation
%

term_subsumer(X,Y,Z) :-
	term_subsumer(X,Y,Z,[],_).

term_subsumer(X,Y,Z,Memo0,Memo) :- 
	(var(X);var(Y)),
	!,
	lookup_memo(X,Y,Z,Memo0,Memo),!.

% identical functors
term_subsumer(X,Y,Z,Memo0,Memo) :-
	functor(X,FX,AX),
	functor(Y,FX,AX),
	!,
	X =.. [_|XArgs],
	Y =.. [_|YArgs],
	term_subsumer_l(XArgs,YArgs,ZArgs,Memo0,Memo),
	Z =.. [FX|ZArgs],
        !.

% non-identical functors
term_subsumer(X,Y,Z,Memo0,Memo) :- 
	%functor(X,FX,AX),
	%functor(Y,FY,AY),
	%(FX \== FY; AX \== AY),
	lookup_memo(X,Y,Z,Memo0,Memo).

term_subsumer_l([],[],[],M,M).
term_subsumer_l([H1|R1],[H2|R2],[H3|R3],Memo0,Memo) :-
	term_subsumer(H1,H2,H3,Memo0,Memo1),
	term_subsumer_l(R1,R2,R3,Memo1,Memo),
	!.

lookup_memo(X,Y,Z,M0,M0) :- 
	tmember(t(X,Y,Z),M0),!.

lookup_memo(X,Y,Z,M0,[t(X,Y,Z)|M0]).

tmember(t(AX,AY,Z),[t(BX,BY,Z)|_]) :- 
	AX == BX, AY == BY,!.
tmember(E,[_|R]) :- tmember(E,R).

subsumes_workaround(X,Y) :-
	%format('testing if ~p subsumed by ~p~n',[X,Y]),
	copy_term(Y,NY),
	X = Y,
	variant(Y,NY),
	!. % extra choice point here somewhere ?!

subsumes_chk_workaround(X,Y) :-
	copy_term(X,NX),
	subsumes_workaround(NX,Y).

%initial_segment(T1,T2) :- initial_segment(T1,T2,nonvar,_),!.

initial_segment(X,Y) :- copy_term(X,Y).

initial_segment(V,_,_,var) :-
	var(V).

initial_segment(_,_,var,var).

initial_segment(T1,T2,nonvar,X) :-
	functor(T1,F,_),
	T1 =.. [_|Args0],
	initial_segment_l(Args0,Args,nonvar,X),
	T2 =.. [F|Args].

initial_segment_l([],[],X,X).
initial_segment_l([H0|R0],[H1|R1],X0,X) :-
	initial_segment(H0,H1,X0,X1),
	initial_segment_l(R0,R1,X1,X).

% from yap manual

list_profile :-
        % get number of calls for each profiled procedure
        setof(D-[M:P|D1],(current_module(M),profile_data(M:P,calls,D),profile_data(M:P,retries,D1)),LP),
        % output so that the most often called
        % predicates will come last:
        write_profile_data(LP).
 
list_profile(Module) :-
        % get number of calls for each profiled procedure
        setof(D-[Module:P|D1],(profile_data(Module:P,calls,D),profile_data(Module:P,retries,D1)),LP),
        % output so that the most often called
        % predicates will come last:
        write_profile_data(LP).
 
write_profile_data([]).
write_profile_data([D-[M:P|R]|SLP]) :-
        % swap the two calls if you want the most often
        %  called predicates first.
        format('~a:~w: ~32+~t~d~12+~t~d~12+~n', [M,P,D,R]),
        write_profile_data(SLP).

% XXX - stupid slow code

subterm_count(T1,T2,N) :- sumnodes(counter(T2),T1,0,N).

counter(T2,ST,N,NN) :- subterm(ST,T2), NN is N + 1, !.

counter(T2,ST,N,N).

subterm(ST,T2) :- sumnodes(checker(ST),T2,false,true).

checker(ST,T,_,true) :- variant(ST,T),!.
checker(ST,T,X,X).



% call init as the last step

% default to depth 1000 searches
fixeddepth(10).

% turn expanding on ... 
expanding.

/*
:- use_module(library(charsio)).
:- use_module('rp2_type.pl').
*/

doargs([RawQuery0]) :-
        atom_to_chars(RawQuery0,RawQuery1),
        read_from_chars(RawQuery1,RawQuery2),
        rewrite_evidential_body(RawQuery2,RawQuery,query),
        rewrite_query(RawQuery,user,Query,yes,
                      Names0,Names,ReportVars),
        Query = richprolog:query(_,_,E,I,_),
        format('~w.~n~w.~n',[E,I]),
        halt.

% :- unix(argv(Q)),doargs(Q).


